(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(g,a,g)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(2) Obligation:

Clauses:

delminA(tree(T76, void, T77), T76, T77).
delminA(tree(T90, T96, T92), T93, tree(T90, T94, T95)) :- delminA(T96, T93, T94).
lessB(0, s(T135)).
lessB(s(T140), s(T141)) :- lessB(T140, T141).
pC(T159, T158, T163, T162) :- lessB(T159, T158).
pC(T159, T158, T163, T162) :- ','(lessB(T159, T158), deleteD(T158, T163, T162)).
pE(T121, T122, T126, T125) :- lessB(T121, T122).
pE(T121, T122, T126, T125) :- ','(lessB(T121, T122), deleteD(T121, T126, T125)).
pF(T198, T199, T182, T181) :- lessB(T198, T199).
pF(T198, T199, T182, T181) :- ','(lessB(T198, T199), deleteD(s(T198), T182, T181)).
pG(T250, T251, T236, T235) :- lessB(T250, T251).
pG(T250, T251, T236, T235) :- ','(lessB(T250, T251), deleteD(s(T251), T236, T235)).
deleteD(T6, tree(T6, void, T7), T7).
deleteD(T10, tree(T10, T11, void), T11).
deleteD(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)).
deleteD(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) :- delminA(T63, T60, T61).
deleteD(T121, tree(T122, T126, T124), tree(T122, T125, T124)) :- pE(T121, T122, T126, T125).
deleteD(T158, tree(T159, T160, T163), tree(T159, T160, T162)) :- pC(T159, T158, T163, T162).
deleteD(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) :- deleteD(0, T182, T181).
deleteD(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) :- pF(T198, T199, T182, T181).
deleteD(T218, tree(T219, T220, T223), tree(T219, T220, T222)) :- pC(T219, T218, T223, T222).
deleteD(s(T241), tree(0, T233, T236), tree(0, T233, T235)) :- deleteD(s(T241), T236, T235).
deleteD(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) :- pG(T250, T251, T236, T235).
deleteD(T265, tree(T265, T266, tree(T279, void, T280)), tree(T279, T266, T280)).
deleteD(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) :- delminA(T311, T308, T309).
deleteD(T336, tree(T337, T341, T339), tree(T337, T340, T339)) :- pE(T336, T337, T341, T340).
deleteD(T354, tree(T355, T356, T359), tree(T355, T356, T358)) :- pC(T355, T354, T359, T358).
deleteD(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) :- deleteD(0, T372, T371).
deleteD(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) :- pF(T388, T389, T372, T371).
deleteD(T402, tree(T403, T404, T407), tree(T403, T404, T406)) :- pC(T403, T402, T407, T406).
deleteD(s(T425), tree(0, T417, T420), tree(0, T417, T419)) :- deleteD(s(T425), T420, T419).
deleteD(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) :- pG(T434, T435, T420, T419).
deleteD(T440, tree(T440, T441, void), T441).
deleteD(T447, tree(T447, T448, tree(T461, void, T462)), tree(T461, T448, T462)).
deleteD(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) :- delminA(T493, T490, T491).
deleteD(T518, tree(T519, T523, T521), tree(T519, T522, T521)) :- pE(T518, T519, T523, T522).
deleteD(T536, tree(T537, T538, T541), tree(T537, T538, T540)) :- pC(T537, T536, T541, T540).
deleteD(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) :- deleteD(0, T554, T553).
deleteD(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) :- pF(T570, T571, T554, T553).
deleteD(T584, tree(T585, T586, T589), tree(T585, T586, T588)) :- pC(T585, T584, T589, T588).
deleteD(s(T607), tree(0, T599, T602), tree(0, T599, T601)) :- deleteD(s(T607), T602, T601).
deleteD(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) :- pG(T616, T617, T602, T601).
deleteD(T625, tree(T625, T626, tree(T639, void, T640)), tree(T639, T626, T640)).
deleteD(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) :- delminA(T671, T668, T669).
deleteD(T696, tree(T697, T701, T699), tree(T697, T700, T699)) :- pE(T696, T697, T701, T700).
deleteD(T714, tree(T715, T716, T719), tree(T715, T716, T718)) :- pC(T715, T714, T719, T718).
deleteD(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) :- deleteD(0, T732, T731).
deleteD(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) :- pF(T748, T749, T732, T731).
deleteD(T762, tree(T763, T764, T767), tree(T763, T764, T766)) :- pC(T763, T762, T767, T766).
deleteD(s(T785), tree(0, T777, T780), tree(0, T777, T779)) :- deleteD(s(T785), T780, T779).
deleteD(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) :- pG(T794, T795, T780, T779).

Query: deleteD(g,a,g)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
deleteD_in: (b,f,b)
delminA_in: (f,b,b)
pE_in: (b,b,f,b)
lessB_in: (b,b)
pC_in: (b,b,f,b)
pF_in: (b,b,f,b)
pG_in: (b,b,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

deleteD_in_gag(T6, tree(T6, void, T7), T7) → deleteD_out_gag(T6, tree(T6, void, T7), T7)
deleteD_in_gag(T10, tree(T10, T11, void), T11) → deleteD_out_gag(T10, tree(T10, T11, void), T11)
deleteD_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → deleteD_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
deleteD_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
delminA_in_agg(tree(T76, void, T77), T76, T77) → delminA_out_agg(tree(T76, void, T77), T76, T77)
delminA_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delminA_out_agg(T96, T93, T94)) → delminA_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_out_agg(T63, T60, T61)) → deleteD_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
deleteD_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_gag(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
pE_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, lessB_in_gg(T121, T122))
lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → pE_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
deleteD_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_gag(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
pC_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → pC_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
deleteD_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_gag(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
deleteD_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_gag(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
pF_in_ggag(T198, T199, T182, T181) → U7_ggag(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → pF_out_ggag(T198, T199, T182, T181)
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_ggag(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
deleteD_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_gag(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
U16_gag(T218, T219, T220, T223, T222, pC_out_ggag(T219, T218, T223, T222)) → deleteD_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
deleteD_in_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_gag(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
deleteD_in_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_gag(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
pG_in_ggag(T250, T251, T236, T235) → U9_ggag(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → pG_out_ggag(T250, T251, T236, T235)
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_ggag(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
deleteD_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_out_agg(T311, T308, T309)) → deleteD_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
deleteD_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_gag(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
U20_gag(T336, T337, T341, T339, T340, pE_out_ggag(T336, T337, T341, T340)) → deleteD_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
deleteD_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_gag(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
U21_gag(T354, T355, T356, T359, T358, pC_out_ggag(T355, T354, T359, T358)) → deleteD_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
deleteD_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_gag(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
deleteD_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_gag(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
U23_gag(T388, T389, T372, T370, T371, pF_out_ggag(T388, T389, T372, T371)) → deleteD_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
deleteD_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_gag(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
U24_gag(T402, T403, T404, T407, T406, pC_out_ggag(T403, T402, T407, T406)) → deleteD_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
deleteD_in_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_gag(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
deleteD_in_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_gag(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
U26_gag(T435, T434, T417, T420, T419, pG_out_ggag(T434, T435, T420, T419)) → deleteD_out_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419))
deleteD_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_out_agg(T493, T490, T491)) → deleteD_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
deleteD_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_gag(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
U28_gag(T518, T519, T523, T521, T522, pE_out_ggag(T518, T519, T523, T522)) → deleteD_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
deleteD_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_gag(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
U29_gag(T536, T537, T538, T541, T540, pC_out_ggag(T537, T536, T541, T540)) → deleteD_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
deleteD_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_gag(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
deleteD_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_gag(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
U31_gag(T570, T571, T554, T552, T553, pF_out_ggag(T570, T571, T554, T553)) → deleteD_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
deleteD_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_gag(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
U32_gag(T584, T585, T586, T589, T588, pC_out_ggag(T585, T584, T589, T588)) → deleteD_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
deleteD_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_gag(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
deleteD_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_gag(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
U34_gag(T617, T616, T599, T602, T601, pG_out_ggag(T616, T617, T602, T601)) → deleteD_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
deleteD_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_out_agg(T671, T668, T669)) → deleteD_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
deleteD_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_gag(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
U36_gag(T696, T697, T701, T699, T700, pE_out_ggag(T696, T697, T701, T700)) → deleteD_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
deleteD_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_gag(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
U37_gag(T714, T715, T716, T719, T718, pC_out_ggag(T715, T714, T719, T718)) → deleteD_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
deleteD_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_gag(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
deleteD_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_gag(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
U39_gag(T748, T749, T732, T730, T731, pF_out_ggag(T748, T749, T732, T731)) → deleteD_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
deleteD_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_gag(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
U40_gag(T762, T763, T764, T767, T766, pC_out_ggag(T763, T762, T767, T766)) → deleteD_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
deleteD_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_gag(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
deleteD_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_gag(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))
U42_gag(T795, T794, T777, T780, T779, pG_out_ggag(T794, T795, T780, T779)) → deleteD_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U41_gag(T785, T777, T780, T779, deleteD_out_gag(s(T785), T780, T779)) → deleteD_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U38_gag(T737, T732, T730, T731, deleteD_out_gag(0, T732, T731)) → deleteD_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U33_gag(T607, T599, T602, T601, deleteD_out_gag(s(T607), T602, T601)) → deleteD_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U30_gag(T559, T554, T552, T553, deleteD_out_gag(0, T554, T553)) → deleteD_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U25_gag(T425, T417, T420, T419, deleteD_out_gag(s(T425), T420, T419)) → deleteD_out_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419))
U22_gag(T377, T372, T370, T371, deleteD_out_gag(0, T372, T371)) → deleteD_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U10_ggag(T250, T251, T236, T235, deleteD_out_gag(s(T251), T236, T235)) → pG_out_ggag(T250, T251, T236, T235)
U18_gag(T251, T250, T233, T236, T235, pG_out_ggag(T250, T251, T236, T235)) → deleteD_out_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235))
U17_gag(T241, T233, T236, T235, deleteD_out_gag(s(T241), T236, T235)) → deleteD_out_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235))
U8_ggag(T198, T199, T182, T181, deleteD_out_gag(s(T198), T182, T181)) → pF_out_ggag(T198, T199, T182, T181)
U15_gag(T198, T199, T182, T180, T181, pF_out_ggag(T198, T199, T182, T181)) → deleteD_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U14_gag(T187, T182, T180, T181, deleteD_out_gag(0, T182, T181)) → deleteD_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, deleteD_out_gag(T158, T163, T162)) → pC_out_ggag(T159, T158, T163, T162)
U13_gag(T158, T159, T160, T163, T162, pC_out_ggag(T159, T158, T163, T162)) → deleteD_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, deleteD_out_gag(T121, T126, T125)) → pE_out_ggag(T121, T122, T126, T125)
U12_gag(T121, T122, T126, T124, T125, pE_out_ggag(T121, T122, T126, T125)) → deleteD_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
deleteD_in_gag(x1, x2, x3)  =  deleteD_in_gag(x1, x3)
deleteD_out_gag(x1, x2, x3)  =  deleteD_out_gag(x1, x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_gag(x1, x2, x3, x6, x7, x8, x9)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
delminA_out_agg(x1, x2, x3)  =  delminA_out_agg(x2, x3)
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x1, x4, x5, x6, x7)
U12_gag(x1, x2, x3, x4, x5, x6)  =  U12_gag(x1, x2, x4, x5, x6)
pE_in_ggag(x1, x2, x3, x4)  =  pE_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x2, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessB_out_gg(x1, x2)  =  lessB_out_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x1, x2, x3)
pE_out_ggag(x1, x2, x3, x4)  =  pE_out_ggag(x1, x2, x4)
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x1, x2, x4, x5)
U13_gag(x1, x2, x3, x4, x5, x6)  =  U13_gag(x1, x2, x3, x5, x6)
pC_in_ggag(x1, x2, x3, x4)  =  pC_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x1, x2, x4, x5)
pC_out_ggag(x1, x2, x3, x4)  =  pC_out_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x1, x2, x4, x5)
U14_gag(x1, x2, x3, x4, x5)  =  U14_gag(x1, x3, x4, x5)
U15_gag(x1, x2, x3, x4, x5, x6)  =  U15_gag(x1, x2, x4, x5, x6)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4, x5)  =  U7_ggag(x1, x2, x4, x5)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x4)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x1, x2, x4, x5)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x1, x2, x3, x5, x6)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x2, x4, x5)
U18_gag(x1, x2, x3, x4, x5, x6)  =  U18_gag(x1, x2, x3, x5, x6)
pG_in_ggag(x1, x2, x3, x4)  =  pG_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x2, x4, x5)
pG_out_ggag(x1, x2, x3, x4)  =  pG_out_ggag(x1, x2, x4)
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x1, x2, x4, x5)
U19_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_gag(x1, x2, x3, x6, x7, x8, x9)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x1, x2, x4, x5, x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x1, x2, x3, x5, x6)
U22_gag(x1, x2, x3, x4, x5)  =  U22_gag(x1, x3, x4, x5)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x1, x2, x4, x5, x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x1, x2, x3, x5, x6)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x1, x2, x4, x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x1, x2, x3, x5, x6)
U27_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_gag(x1, x2, x3, x6, x7, x8, x9)
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x1, x2, x4, x5, x6)
U29_gag(x1, x2, x3, x4, x5, x6)  =  U29_gag(x1, x2, x3, x5, x6)
U30_gag(x1, x2, x3, x4, x5)  =  U30_gag(x1, x3, x4, x5)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x1, x2, x4, x5, x6)
U32_gag(x1, x2, x3, x4, x5, x6)  =  U32_gag(x1, x2, x3, x5, x6)
U33_gag(x1, x2, x3, x4, x5)  =  U33_gag(x1, x2, x4, x5)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x1, x2, x3, x5, x6)
U35_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_gag(x1, x2, x3, x6, x7, x8, x9)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x1, x2, x4, x5, x6)
U37_gag(x1, x2, x3, x4, x5, x6)  =  U37_gag(x1, x2, x3, x5, x6)
U38_gag(x1, x2, x3, x4, x5)  =  U38_gag(x1, x3, x4, x5)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x1, x2, x4, x5, x6)
U40_gag(x1, x2, x3, x4, x5, x6)  =  U40_gag(x1, x2, x3, x5, x6)
U41_gag(x1, x2, x3, x4, x5)  =  U41_gag(x1, x2, x4, x5)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x1, x2, x3, x5, x6)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

deleteD_in_gag(T6, tree(T6, void, T7), T7) → deleteD_out_gag(T6, tree(T6, void, T7), T7)
deleteD_in_gag(T10, tree(T10, T11, void), T11) → deleteD_out_gag(T10, tree(T10, T11, void), T11)
deleteD_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → deleteD_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
deleteD_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
delminA_in_agg(tree(T76, void, T77), T76, T77) → delminA_out_agg(tree(T76, void, T77), T76, T77)
delminA_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delminA_out_agg(T96, T93, T94)) → delminA_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_out_agg(T63, T60, T61)) → deleteD_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
deleteD_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_gag(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
pE_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, lessB_in_gg(T121, T122))
lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → pE_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
deleteD_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_gag(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
pC_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → pC_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
deleteD_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_gag(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
deleteD_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_gag(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
pF_in_ggag(T198, T199, T182, T181) → U7_ggag(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → pF_out_ggag(T198, T199, T182, T181)
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_ggag(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
deleteD_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_gag(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
U16_gag(T218, T219, T220, T223, T222, pC_out_ggag(T219, T218, T223, T222)) → deleteD_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
deleteD_in_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_gag(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
deleteD_in_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_gag(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
pG_in_ggag(T250, T251, T236, T235) → U9_ggag(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → pG_out_ggag(T250, T251, T236, T235)
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_ggag(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
deleteD_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_out_agg(T311, T308, T309)) → deleteD_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
deleteD_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_gag(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
U20_gag(T336, T337, T341, T339, T340, pE_out_ggag(T336, T337, T341, T340)) → deleteD_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
deleteD_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_gag(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
U21_gag(T354, T355, T356, T359, T358, pC_out_ggag(T355, T354, T359, T358)) → deleteD_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
deleteD_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_gag(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
deleteD_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_gag(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
U23_gag(T388, T389, T372, T370, T371, pF_out_ggag(T388, T389, T372, T371)) → deleteD_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
deleteD_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_gag(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
U24_gag(T402, T403, T404, T407, T406, pC_out_ggag(T403, T402, T407, T406)) → deleteD_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
deleteD_in_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_gag(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
deleteD_in_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_gag(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
U26_gag(T435, T434, T417, T420, T419, pG_out_ggag(T434, T435, T420, T419)) → deleteD_out_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419))
deleteD_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_out_agg(T493, T490, T491)) → deleteD_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
deleteD_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_gag(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
U28_gag(T518, T519, T523, T521, T522, pE_out_ggag(T518, T519, T523, T522)) → deleteD_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
deleteD_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_gag(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
U29_gag(T536, T537, T538, T541, T540, pC_out_ggag(T537, T536, T541, T540)) → deleteD_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
deleteD_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_gag(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
deleteD_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_gag(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
U31_gag(T570, T571, T554, T552, T553, pF_out_ggag(T570, T571, T554, T553)) → deleteD_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
deleteD_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_gag(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
U32_gag(T584, T585, T586, T589, T588, pC_out_ggag(T585, T584, T589, T588)) → deleteD_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
deleteD_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_gag(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
deleteD_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_gag(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
U34_gag(T617, T616, T599, T602, T601, pG_out_ggag(T616, T617, T602, T601)) → deleteD_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
deleteD_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_out_agg(T671, T668, T669)) → deleteD_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
deleteD_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_gag(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
U36_gag(T696, T697, T701, T699, T700, pE_out_ggag(T696, T697, T701, T700)) → deleteD_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
deleteD_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_gag(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
U37_gag(T714, T715, T716, T719, T718, pC_out_ggag(T715, T714, T719, T718)) → deleteD_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
deleteD_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_gag(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
deleteD_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_gag(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
U39_gag(T748, T749, T732, T730, T731, pF_out_ggag(T748, T749, T732, T731)) → deleteD_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
deleteD_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_gag(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
U40_gag(T762, T763, T764, T767, T766, pC_out_ggag(T763, T762, T767, T766)) → deleteD_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
deleteD_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_gag(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
deleteD_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_gag(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))
U42_gag(T795, T794, T777, T780, T779, pG_out_ggag(T794, T795, T780, T779)) → deleteD_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U41_gag(T785, T777, T780, T779, deleteD_out_gag(s(T785), T780, T779)) → deleteD_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U38_gag(T737, T732, T730, T731, deleteD_out_gag(0, T732, T731)) → deleteD_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U33_gag(T607, T599, T602, T601, deleteD_out_gag(s(T607), T602, T601)) → deleteD_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U30_gag(T559, T554, T552, T553, deleteD_out_gag(0, T554, T553)) → deleteD_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U25_gag(T425, T417, T420, T419, deleteD_out_gag(s(T425), T420, T419)) → deleteD_out_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419))
U22_gag(T377, T372, T370, T371, deleteD_out_gag(0, T372, T371)) → deleteD_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U10_ggag(T250, T251, T236, T235, deleteD_out_gag(s(T251), T236, T235)) → pG_out_ggag(T250, T251, T236, T235)
U18_gag(T251, T250, T233, T236, T235, pG_out_ggag(T250, T251, T236, T235)) → deleteD_out_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235))
U17_gag(T241, T233, T236, T235, deleteD_out_gag(s(T241), T236, T235)) → deleteD_out_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235))
U8_ggag(T198, T199, T182, T181, deleteD_out_gag(s(T198), T182, T181)) → pF_out_ggag(T198, T199, T182, T181)
U15_gag(T198, T199, T182, T180, T181, pF_out_ggag(T198, T199, T182, T181)) → deleteD_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U14_gag(T187, T182, T180, T181, deleteD_out_gag(0, T182, T181)) → deleteD_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, deleteD_out_gag(T158, T163, T162)) → pC_out_ggag(T159, T158, T163, T162)
U13_gag(T158, T159, T160, T163, T162, pC_out_ggag(T159, T158, T163, T162)) → deleteD_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, deleteD_out_gag(T121, T126, T125)) → pE_out_ggag(T121, T122, T126, T125)
U12_gag(T121, T122, T126, T124, T125, pE_out_ggag(T121, T122, T126, T125)) → deleteD_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
deleteD_in_gag(x1, x2, x3)  =  deleteD_in_gag(x1, x3)
deleteD_out_gag(x1, x2, x3)  =  deleteD_out_gag(x1, x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_gag(x1, x2, x3, x6, x7, x8, x9)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
delminA_out_agg(x1, x2, x3)  =  delminA_out_agg(x2, x3)
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x1, x4, x5, x6, x7)
U12_gag(x1, x2, x3, x4, x5, x6)  =  U12_gag(x1, x2, x4, x5, x6)
pE_in_ggag(x1, x2, x3, x4)  =  pE_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x2, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessB_out_gg(x1, x2)  =  lessB_out_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x1, x2, x3)
pE_out_ggag(x1, x2, x3, x4)  =  pE_out_ggag(x1, x2, x4)
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x1, x2, x4, x5)
U13_gag(x1, x2, x3, x4, x5, x6)  =  U13_gag(x1, x2, x3, x5, x6)
pC_in_ggag(x1, x2, x3, x4)  =  pC_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x1, x2, x4, x5)
pC_out_ggag(x1, x2, x3, x4)  =  pC_out_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x1, x2, x4, x5)
U14_gag(x1, x2, x3, x4, x5)  =  U14_gag(x1, x3, x4, x5)
U15_gag(x1, x2, x3, x4, x5, x6)  =  U15_gag(x1, x2, x4, x5, x6)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4, x5)  =  U7_ggag(x1, x2, x4, x5)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x4)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x1, x2, x4, x5)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x1, x2, x3, x5, x6)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x2, x4, x5)
U18_gag(x1, x2, x3, x4, x5, x6)  =  U18_gag(x1, x2, x3, x5, x6)
pG_in_ggag(x1, x2, x3, x4)  =  pG_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x2, x4, x5)
pG_out_ggag(x1, x2, x3, x4)  =  pG_out_ggag(x1, x2, x4)
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x1, x2, x4, x5)
U19_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_gag(x1, x2, x3, x6, x7, x8, x9)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x1, x2, x4, x5, x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x1, x2, x3, x5, x6)
U22_gag(x1, x2, x3, x4, x5)  =  U22_gag(x1, x3, x4, x5)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x1, x2, x4, x5, x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x1, x2, x3, x5, x6)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x1, x2, x4, x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x1, x2, x3, x5, x6)
U27_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_gag(x1, x2, x3, x6, x7, x8, x9)
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x1, x2, x4, x5, x6)
U29_gag(x1, x2, x3, x4, x5, x6)  =  U29_gag(x1, x2, x3, x5, x6)
U30_gag(x1, x2, x3, x4, x5)  =  U30_gag(x1, x3, x4, x5)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x1, x2, x4, x5, x6)
U32_gag(x1, x2, x3, x4, x5, x6)  =  U32_gag(x1, x2, x3, x5, x6)
U33_gag(x1, x2, x3, x4, x5)  =  U33_gag(x1, x2, x4, x5)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x1, x2, x3, x5, x6)
U35_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_gag(x1, x2, x3, x6, x7, x8, x9)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x1, x2, x4, x5, x6)
U37_gag(x1, x2, x3, x4, x5, x6)  =  U37_gag(x1, x2, x3, x5, x6)
U38_gag(x1, x2, x3, x4, x5)  =  U38_gag(x1, x3, x4, x5)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x1, x2, x4, x5, x6)
U40_gag(x1, x2, x3, x4, x5, x6)  =  U40_gag(x1, x2, x3, x5, x6)
U41_gag(x1, x2, x3, x4, x5)  =  U41_gag(x1, x2, x4, x5)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x1, x2, x3, x5, x6)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

DELETED_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_GAG(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
DELETED_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMINA_IN_AGG(T63, T60, T61)
DELMINA_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_AGG(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
DELMINA_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMINA_IN_AGG(T96, T93, T94)
DELETED_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_GAG(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
DELETED_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → PE_IN_GGAG(T121, T122, T126, T125)
PE_IN_GGAG(T121, T122, T126, T125) → U5_GGAG(T121, T122, T126, T125, lessB_in_gg(T121, T122))
PE_IN_GGAG(T121, T122, T126, T125) → LESSB_IN_GG(T121, T122)
LESSB_IN_GG(s(T140), s(T141)) → U2_GG(T140, T141, lessB_in_gg(T140, T141))
LESSB_IN_GG(s(T140), s(T141)) → LESSB_IN_GG(T140, T141)
U5_GGAG(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_GGAG(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
U5_GGAG(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → DELETED_IN_GAG(T121, T126, T125)
DELETED_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_GAG(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
DELETED_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → PC_IN_GGAG(T159, T158, T163, T162)
PC_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, lessB_in_gg(T159, T158))
PC_IN_GGAG(T159, T158, T163, T162) → LESSB_IN_GG(T159, T158)
U3_GGAG(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_GGAG(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
U3_GGAG(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → DELETED_IN_GAG(T158, T163, T162)
DELETED_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_GAG(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
DELETED_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETED_IN_GAG(0, T182, T181)
DELETED_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_GAG(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
DELETED_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → PF_IN_GGAG(T198, T199, T182, T181)
PF_IN_GGAG(T198, T199, T182, T181) → U7_GGAG(T198, T199, T182, T181, lessB_in_gg(T198, T199))
PF_IN_GGAG(T198, T199, T182, T181) → LESSB_IN_GG(T198, T199)
U7_GGAG(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_GGAG(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
U7_GGAG(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → DELETED_IN_GAG(s(T198), T182, T181)
DELETED_IN_GAG(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_GAG(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
DELETED_IN_GAG(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_GAG(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
DELETED_IN_GAG(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → DELETED_IN_GAG(s(T241), T236, T235)
DELETED_IN_GAG(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_GAG(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
DELETED_IN_GAG(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → PG_IN_GGAG(T250, T251, T236, T235)
PG_IN_GGAG(T250, T251, T236, T235) → U9_GGAG(T250, T251, T236, T235, lessB_in_gg(T250, T251))
PG_IN_GGAG(T250, T251, T236, T235) → LESSB_IN_GG(T250, T251)
U9_GGAG(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_GGAG(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
U9_GGAG(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → DELETED_IN_GAG(s(T251), T236, T235)
DELETED_IN_GAG(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_GAG(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
DELETED_IN_GAG(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_GAG(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
DELETED_IN_GAG(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_GAG(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
DELETED_IN_GAG(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_GAG(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
DELETED_IN_GAG(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_GAG(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
DELETED_IN_GAG(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_GAG(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
DELETED_IN_GAG(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_GAG(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
DELETED_IN_GAG(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_GAG(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
DELETED_IN_GAG(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_GAG(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
DELETED_IN_GAG(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_GAG(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
DELETED_IN_GAG(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_GAG(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
DELETED_IN_GAG(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_GAG(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
DELETED_IN_GAG(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_GAG(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
DELETED_IN_GAG(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_GAG(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
DELETED_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_GAG(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
DELETED_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_GAG(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
DELETED_IN_GAG(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_GAG(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
DELETED_IN_GAG(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_GAG(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
DELETED_IN_GAG(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_GAG(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
DELETED_IN_GAG(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_GAG(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
DELETED_IN_GAG(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_GAG(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
DELETED_IN_GAG(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_GAG(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
DELETED_IN_GAG(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_GAG(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
DELETED_IN_GAG(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_GAG(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))

The TRS R consists of the following rules:

deleteD_in_gag(T6, tree(T6, void, T7), T7) → deleteD_out_gag(T6, tree(T6, void, T7), T7)
deleteD_in_gag(T10, tree(T10, T11, void), T11) → deleteD_out_gag(T10, tree(T10, T11, void), T11)
deleteD_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → deleteD_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
deleteD_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
delminA_in_agg(tree(T76, void, T77), T76, T77) → delminA_out_agg(tree(T76, void, T77), T76, T77)
delminA_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delminA_out_agg(T96, T93, T94)) → delminA_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_out_agg(T63, T60, T61)) → deleteD_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
deleteD_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_gag(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
pE_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, lessB_in_gg(T121, T122))
lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → pE_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
deleteD_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_gag(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
pC_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → pC_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
deleteD_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_gag(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
deleteD_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_gag(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
pF_in_ggag(T198, T199, T182, T181) → U7_ggag(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → pF_out_ggag(T198, T199, T182, T181)
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_ggag(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
deleteD_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_gag(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
U16_gag(T218, T219, T220, T223, T222, pC_out_ggag(T219, T218, T223, T222)) → deleteD_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
deleteD_in_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_gag(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
deleteD_in_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_gag(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
pG_in_ggag(T250, T251, T236, T235) → U9_ggag(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → pG_out_ggag(T250, T251, T236, T235)
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_ggag(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
deleteD_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_out_agg(T311, T308, T309)) → deleteD_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
deleteD_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_gag(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
U20_gag(T336, T337, T341, T339, T340, pE_out_ggag(T336, T337, T341, T340)) → deleteD_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
deleteD_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_gag(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
U21_gag(T354, T355, T356, T359, T358, pC_out_ggag(T355, T354, T359, T358)) → deleteD_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
deleteD_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_gag(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
deleteD_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_gag(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
U23_gag(T388, T389, T372, T370, T371, pF_out_ggag(T388, T389, T372, T371)) → deleteD_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
deleteD_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_gag(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
U24_gag(T402, T403, T404, T407, T406, pC_out_ggag(T403, T402, T407, T406)) → deleteD_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
deleteD_in_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_gag(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
deleteD_in_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_gag(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
U26_gag(T435, T434, T417, T420, T419, pG_out_ggag(T434, T435, T420, T419)) → deleteD_out_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419))
deleteD_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_out_agg(T493, T490, T491)) → deleteD_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
deleteD_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_gag(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
U28_gag(T518, T519, T523, T521, T522, pE_out_ggag(T518, T519, T523, T522)) → deleteD_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
deleteD_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_gag(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
U29_gag(T536, T537, T538, T541, T540, pC_out_ggag(T537, T536, T541, T540)) → deleteD_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
deleteD_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_gag(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
deleteD_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_gag(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
U31_gag(T570, T571, T554, T552, T553, pF_out_ggag(T570, T571, T554, T553)) → deleteD_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
deleteD_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_gag(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
U32_gag(T584, T585, T586, T589, T588, pC_out_ggag(T585, T584, T589, T588)) → deleteD_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
deleteD_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_gag(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
deleteD_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_gag(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
U34_gag(T617, T616, T599, T602, T601, pG_out_ggag(T616, T617, T602, T601)) → deleteD_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
deleteD_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_out_agg(T671, T668, T669)) → deleteD_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
deleteD_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_gag(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
U36_gag(T696, T697, T701, T699, T700, pE_out_ggag(T696, T697, T701, T700)) → deleteD_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
deleteD_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_gag(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
U37_gag(T714, T715, T716, T719, T718, pC_out_ggag(T715, T714, T719, T718)) → deleteD_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
deleteD_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_gag(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
deleteD_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_gag(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
U39_gag(T748, T749, T732, T730, T731, pF_out_ggag(T748, T749, T732, T731)) → deleteD_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
deleteD_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_gag(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
U40_gag(T762, T763, T764, T767, T766, pC_out_ggag(T763, T762, T767, T766)) → deleteD_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
deleteD_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_gag(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
deleteD_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_gag(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))
U42_gag(T795, T794, T777, T780, T779, pG_out_ggag(T794, T795, T780, T779)) → deleteD_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U41_gag(T785, T777, T780, T779, deleteD_out_gag(s(T785), T780, T779)) → deleteD_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U38_gag(T737, T732, T730, T731, deleteD_out_gag(0, T732, T731)) → deleteD_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U33_gag(T607, T599, T602, T601, deleteD_out_gag(s(T607), T602, T601)) → deleteD_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U30_gag(T559, T554, T552, T553, deleteD_out_gag(0, T554, T553)) → deleteD_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U25_gag(T425, T417, T420, T419, deleteD_out_gag(s(T425), T420, T419)) → deleteD_out_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419))
U22_gag(T377, T372, T370, T371, deleteD_out_gag(0, T372, T371)) → deleteD_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U10_ggag(T250, T251, T236, T235, deleteD_out_gag(s(T251), T236, T235)) → pG_out_ggag(T250, T251, T236, T235)
U18_gag(T251, T250, T233, T236, T235, pG_out_ggag(T250, T251, T236, T235)) → deleteD_out_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235))
U17_gag(T241, T233, T236, T235, deleteD_out_gag(s(T241), T236, T235)) → deleteD_out_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235))
U8_ggag(T198, T199, T182, T181, deleteD_out_gag(s(T198), T182, T181)) → pF_out_ggag(T198, T199, T182, T181)
U15_gag(T198, T199, T182, T180, T181, pF_out_ggag(T198, T199, T182, T181)) → deleteD_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U14_gag(T187, T182, T180, T181, deleteD_out_gag(0, T182, T181)) → deleteD_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, deleteD_out_gag(T158, T163, T162)) → pC_out_ggag(T159, T158, T163, T162)
U13_gag(T158, T159, T160, T163, T162, pC_out_ggag(T159, T158, T163, T162)) → deleteD_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, deleteD_out_gag(T121, T126, T125)) → pE_out_ggag(T121, T122, T126, T125)
U12_gag(T121, T122, T126, T124, T125, pE_out_ggag(T121, T122, T126, T125)) → deleteD_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
deleteD_in_gag(x1, x2, x3)  =  deleteD_in_gag(x1, x3)
deleteD_out_gag(x1, x2, x3)  =  deleteD_out_gag(x1, x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_gag(x1, x2, x3, x6, x7, x8, x9)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
delminA_out_agg(x1, x2, x3)  =  delminA_out_agg(x2, x3)
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x1, x4, x5, x6, x7)
U12_gag(x1, x2, x3, x4, x5, x6)  =  U12_gag(x1, x2, x4, x5, x6)
pE_in_ggag(x1, x2, x3, x4)  =  pE_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x2, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessB_out_gg(x1, x2)  =  lessB_out_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x1, x2, x3)
pE_out_ggag(x1, x2, x3, x4)  =  pE_out_ggag(x1, x2, x4)
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x1, x2, x4, x5)
U13_gag(x1, x2, x3, x4, x5, x6)  =  U13_gag(x1, x2, x3, x5, x6)
pC_in_ggag(x1, x2, x3, x4)  =  pC_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x1, x2, x4, x5)
pC_out_ggag(x1, x2, x3, x4)  =  pC_out_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x1, x2, x4, x5)
U14_gag(x1, x2, x3, x4, x5)  =  U14_gag(x1, x3, x4, x5)
U15_gag(x1, x2, x3, x4, x5, x6)  =  U15_gag(x1, x2, x4, x5, x6)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4, x5)  =  U7_ggag(x1, x2, x4, x5)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x4)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x1, x2, x4, x5)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x1, x2, x3, x5, x6)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x2, x4, x5)
U18_gag(x1, x2, x3, x4, x5, x6)  =  U18_gag(x1, x2, x3, x5, x6)
pG_in_ggag(x1, x2, x3, x4)  =  pG_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x2, x4, x5)
pG_out_ggag(x1, x2, x3, x4)  =  pG_out_ggag(x1, x2, x4)
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x1, x2, x4, x5)
U19_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_gag(x1, x2, x3, x6, x7, x8, x9)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x1, x2, x4, x5, x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x1, x2, x3, x5, x6)
U22_gag(x1, x2, x3, x4, x5)  =  U22_gag(x1, x3, x4, x5)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x1, x2, x4, x5, x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x1, x2, x3, x5, x6)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x1, x2, x4, x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x1, x2, x3, x5, x6)
U27_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_gag(x1, x2, x3, x6, x7, x8, x9)
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x1, x2, x4, x5, x6)
U29_gag(x1, x2, x3, x4, x5, x6)  =  U29_gag(x1, x2, x3, x5, x6)
U30_gag(x1, x2, x3, x4, x5)  =  U30_gag(x1, x3, x4, x5)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x1, x2, x4, x5, x6)
U32_gag(x1, x2, x3, x4, x5, x6)  =  U32_gag(x1, x2, x3, x5, x6)
U33_gag(x1, x2, x3, x4, x5)  =  U33_gag(x1, x2, x4, x5)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x1, x2, x3, x5, x6)
U35_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_gag(x1, x2, x3, x6, x7, x8, x9)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x1, x2, x4, x5, x6)
U37_gag(x1, x2, x3, x4, x5, x6)  =  U37_gag(x1, x2, x3, x5, x6)
U38_gag(x1, x2, x3, x4, x5)  =  U38_gag(x1, x3, x4, x5)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x1, x2, x4, x5, x6)
U40_gag(x1, x2, x3, x4, x5, x6)  =  U40_gag(x1, x2, x3, x5, x6)
U41_gag(x1, x2, x3, x4, x5)  =  U41_gag(x1, x2, x4, x5)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x1, x2, x3, x5, x6)
DELETED_IN_GAG(x1, x2, x3)  =  DELETED_IN_GAG(x1, x3)
U11_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_GAG(x1, x2, x3, x6, x7, x8, x9)
DELMINA_IN_AGG(x1, x2, x3)  =  DELMINA_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AGG(x1, x4, x5, x6, x7)
U12_GAG(x1, x2, x3, x4, x5, x6)  =  U12_GAG(x1, x2, x4, x5, x6)
PE_IN_GGAG(x1, x2, x3, x4)  =  PE_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x2, x4, x5)
LESSB_IN_GG(x1, x2)  =  LESSB_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U6_GGAG(x1, x2, x3, x4, x5)  =  U6_GGAG(x1, x2, x4, x5)
U13_GAG(x1, x2, x3, x4, x5, x6)  =  U13_GAG(x1, x2, x3, x5, x6)
PC_IN_GGAG(x1, x2, x3, x4)  =  PC_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5)  =  U3_GGAG(x1, x2, x4, x5)
U4_GGAG(x1, x2, x3, x4, x5)  =  U4_GGAG(x1, x2, x4, x5)
U14_GAG(x1, x2, x3, x4, x5)  =  U14_GAG(x1, x3, x4, x5)
U15_GAG(x1, x2, x3, x4, x5, x6)  =  U15_GAG(x1, x2, x4, x5, x6)
PF_IN_GGAG(x1, x2, x3, x4)  =  PF_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4, x5)  =  U7_GGAG(x1, x2, x4, x5)
U8_GGAG(x1, x2, x3, x4, x5)  =  U8_GGAG(x1, x2, x4, x5)
U16_GAG(x1, x2, x3, x4, x5, x6)  =  U16_GAG(x1, x2, x3, x5, x6)
U17_GAG(x1, x2, x3, x4, x5)  =  U17_GAG(x1, x2, x4, x5)
U18_GAG(x1, x2, x3, x4, x5, x6)  =  U18_GAG(x1, x2, x3, x5, x6)
PG_IN_GGAG(x1, x2, x3, x4)  =  PG_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x2, x4, x5)
U10_GGAG(x1, x2, x3, x4, x5)  =  U10_GGAG(x1, x2, x4, x5)
U19_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_GAG(x1, x2, x3, x6, x7, x8, x9)
U20_GAG(x1, x2, x3, x4, x5, x6)  =  U20_GAG(x1, x2, x4, x5, x6)
U21_GAG(x1, x2, x3, x4, x5, x6)  =  U21_GAG(x1, x2, x3, x5, x6)
U22_GAG(x1, x2, x3, x4, x5)  =  U22_GAG(x1, x3, x4, x5)
U23_GAG(x1, x2, x3, x4, x5, x6)  =  U23_GAG(x1, x2, x4, x5, x6)
U24_GAG(x1, x2, x3, x4, x5, x6)  =  U24_GAG(x1, x2, x3, x5, x6)
U25_GAG(x1, x2, x3, x4, x5)  =  U25_GAG(x1, x2, x4, x5)
U26_GAG(x1, x2, x3, x4, x5, x6)  =  U26_GAG(x1, x2, x3, x5, x6)
U27_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_GAG(x1, x2, x3, x6, x7, x8, x9)
U28_GAG(x1, x2, x3, x4, x5, x6)  =  U28_GAG(x1, x2, x4, x5, x6)
U29_GAG(x1, x2, x3, x4, x5, x6)  =  U29_GAG(x1, x2, x3, x5, x6)
U30_GAG(x1, x2, x3, x4, x5)  =  U30_GAG(x1, x3, x4, x5)
U31_GAG(x1, x2, x3, x4, x5, x6)  =  U31_GAG(x1, x2, x4, x5, x6)
U32_GAG(x1, x2, x3, x4, x5, x6)  =  U32_GAG(x1, x2, x3, x5, x6)
U33_GAG(x1, x2, x3, x4, x5)  =  U33_GAG(x1, x2, x4, x5)
U34_GAG(x1, x2, x3, x4, x5, x6)  =  U34_GAG(x1, x2, x3, x5, x6)
U35_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_GAG(x1, x2, x3, x6, x7, x8, x9)
U36_GAG(x1, x2, x3, x4, x5, x6)  =  U36_GAG(x1, x2, x4, x5, x6)
U37_GAG(x1, x2, x3, x4, x5, x6)  =  U37_GAG(x1, x2, x3, x5, x6)
U38_GAG(x1, x2, x3, x4, x5)  =  U38_GAG(x1, x3, x4, x5)
U39_GAG(x1, x2, x3, x4, x5, x6)  =  U39_GAG(x1, x2, x4, x5, x6)
U40_GAG(x1, x2, x3, x4, x5, x6)  =  U40_GAG(x1, x2, x3, x5, x6)
U41_GAG(x1, x2, x3, x4, x5)  =  U41_GAG(x1, x2, x4, x5)
U42_GAG(x1, x2, x3, x4, x5, x6)  =  U42_GAG(x1, x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETED_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_GAG(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
DELETED_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMINA_IN_AGG(T63, T60, T61)
DELMINA_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_AGG(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
DELMINA_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMINA_IN_AGG(T96, T93, T94)
DELETED_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_GAG(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
DELETED_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → PE_IN_GGAG(T121, T122, T126, T125)
PE_IN_GGAG(T121, T122, T126, T125) → U5_GGAG(T121, T122, T126, T125, lessB_in_gg(T121, T122))
PE_IN_GGAG(T121, T122, T126, T125) → LESSB_IN_GG(T121, T122)
LESSB_IN_GG(s(T140), s(T141)) → U2_GG(T140, T141, lessB_in_gg(T140, T141))
LESSB_IN_GG(s(T140), s(T141)) → LESSB_IN_GG(T140, T141)
U5_GGAG(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_GGAG(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
U5_GGAG(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → DELETED_IN_GAG(T121, T126, T125)
DELETED_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_GAG(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
DELETED_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → PC_IN_GGAG(T159, T158, T163, T162)
PC_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, lessB_in_gg(T159, T158))
PC_IN_GGAG(T159, T158, T163, T162) → LESSB_IN_GG(T159, T158)
U3_GGAG(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_GGAG(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
U3_GGAG(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → DELETED_IN_GAG(T158, T163, T162)
DELETED_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_GAG(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
DELETED_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETED_IN_GAG(0, T182, T181)
DELETED_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_GAG(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
DELETED_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → PF_IN_GGAG(T198, T199, T182, T181)
PF_IN_GGAG(T198, T199, T182, T181) → U7_GGAG(T198, T199, T182, T181, lessB_in_gg(T198, T199))
PF_IN_GGAG(T198, T199, T182, T181) → LESSB_IN_GG(T198, T199)
U7_GGAG(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_GGAG(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
U7_GGAG(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → DELETED_IN_GAG(s(T198), T182, T181)
DELETED_IN_GAG(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_GAG(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
DELETED_IN_GAG(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_GAG(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
DELETED_IN_GAG(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → DELETED_IN_GAG(s(T241), T236, T235)
DELETED_IN_GAG(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_GAG(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
DELETED_IN_GAG(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → PG_IN_GGAG(T250, T251, T236, T235)
PG_IN_GGAG(T250, T251, T236, T235) → U9_GGAG(T250, T251, T236, T235, lessB_in_gg(T250, T251))
PG_IN_GGAG(T250, T251, T236, T235) → LESSB_IN_GG(T250, T251)
U9_GGAG(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_GGAG(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
U9_GGAG(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → DELETED_IN_GAG(s(T251), T236, T235)
DELETED_IN_GAG(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_GAG(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
DELETED_IN_GAG(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_GAG(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
DELETED_IN_GAG(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_GAG(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
DELETED_IN_GAG(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_GAG(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
DELETED_IN_GAG(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_GAG(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
DELETED_IN_GAG(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_GAG(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
DELETED_IN_GAG(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_GAG(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
DELETED_IN_GAG(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_GAG(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
DELETED_IN_GAG(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_GAG(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
DELETED_IN_GAG(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_GAG(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
DELETED_IN_GAG(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_GAG(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
DELETED_IN_GAG(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_GAG(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
DELETED_IN_GAG(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_GAG(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
DELETED_IN_GAG(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_GAG(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
DELETED_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_GAG(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
DELETED_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_GAG(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
DELETED_IN_GAG(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_GAG(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
DELETED_IN_GAG(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_GAG(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
DELETED_IN_GAG(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_GAG(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
DELETED_IN_GAG(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_GAG(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
DELETED_IN_GAG(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_GAG(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
DELETED_IN_GAG(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_GAG(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
DELETED_IN_GAG(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_GAG(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
DELETED_IN_GAG(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_GAG(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))

The TRS R consists of the following rules:

deleteD_in_gag(T6, tree(T6, void, T7), T7) → deleteD_out_gag(T6, tree(T6, void, T7), T7)
deleteD_in_gag(T10, tree(T10, T11, void), T11) → deleteD_out_gag(T10, tree(T10, T11, void), T11)
deleteD_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → deleteD_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
deleteD_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
delminA_in_agg(tree(T76, void, T77), T76, T77) → delminA_out_agg(tree(T76, void, T77), T76, T77)
delminA_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delminA_out_agg(T96, T93, T94)) → delminA_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_out_agg(T63, T60, T61)) → deleteD_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
deleteD_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_gag(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
pE_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, lessB_in_gg(T121, T122))
lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → pE_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
deleteD_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_gag(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
pC_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → pC_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
deleteD_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_gag(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
deleteD_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_gag(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
pF_in_ggag(T198, T199, T182, T181) → U7_ggag(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → pF_out_ggag(T198, T199, T182, T181)
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_ggag(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
deleteD_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_gag(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
U16_gag(T218, T219, T220, T223, T222, pC_out_ggag(T219, T218, T223, T222)) → deleteD_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
deleteD_in_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_gag(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
deleteD_in_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_gag(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
pG_in_ggag(T250, T251, T236, T235) → U9_ggag(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → pG_out_ggag(T250, T251, T236, T235)
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_ggag(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
deleteD_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_out_agg(T311, T308, T309)) → deleteD_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
deleteD_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_gag(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
U20_gag(T336, T337, T341, T339, T340, pE_out_ggag(T336, T337, T341, T340)) → deleteD_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
deleteD_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_gag(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
U21_gag(T354, T355, T356, T359, T358, pC_out_ggag(T355, T354, T359, T358)) → deleteD_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
deleteD_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_gag(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
deleteD_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_gag(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
U23_gag(T388, T389, T372, T370, T371, pF_out_ggag(T388, T389, T372, T371)) → deleteD_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
deleteD_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_gag(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
U24_gag(T402, T403, T404, T407, T406, pC_out_ggag(T403, T402, T407, T406)) → deleteD_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
deleteD_in_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_gag(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
deleteD_in_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_gag(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
U26_gag(T435, T434, T417, T420, T419, pG_out_ggag(T434, T435, T420, T419)) → deleteD_out_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419))
deleteD_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_out_agg(T493, T490, T491)) → deleteD_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
deleteD_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_gag(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
U28_gag(T518, T519, T523, T521, T522, pE_out_ggag(T518, T519, T523, T522)) → deleteD_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
deleteD_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_gag(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
U29_gag(T536, T537, T538, T541, T540, pC_out_ggag(T537, T536, T541, T540)) → deleteD_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
deleteD_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_gag(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
deleteD_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_gag(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
U31_gag(T570, T571, T554, T552, T553, pF_out_ggag(T570, T571, T554, T553)) → deleteD_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
deleteD_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_gag(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
U32_gag(T584, T585, T586, T589, T588, pC_out_ggag(T585, T584, T589, T588)) → deleteD_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
deleteD_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_gag(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
deleteD_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_gag(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
U34_gag(T617, T616, T599, T602, T601, pG_out_ggag(T616, T617, T602, T601)) → deleteD_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
deleteD_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_out_agg(T671, T668, T669)) → deleteD_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
deleteD_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_gag(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
U36_gag(T696, T697, T701, T699, T700, pE_out_ggag(T696, T697, T701, T700)) → deleteD_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
deleteD_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_gag(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
U37_gag(T714, T715, T716, T719, T718, pC_out_ggag(T715, T714, T719, T718)) → deleteD_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
deleteD_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_gag(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
deleteD_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_gag(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
U39_gag(T748, T749, T732, T730, T731, pF_out_ggag(T748, T749, T732, T731)) → deleteD_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
deleteD_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_gag(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
U40_gag(T762, T763, T764, T767, T766, pC_out_ggag(T763, T762, T767, T766)) → deleteD_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
deleteD_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_gag(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
deleteD_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_gag(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))
U42_gag(T795, T794, T777, T780, T779, pG_out_ggag(T794, T795, T780, T779)) → deleteD_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U41_gag(T785, T777, T780, T779, deleteD_out_gag(s(T785), T780, T779)) → deleteD_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U38_gag(T737, T732, T730, T731, deleteD_out_gag(0, T732, T731)) → deleteD_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U33_gag(T607, T599, T602, T601, deleteD_out_gag(s(T607), T602, T601)) → deleteD_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U30_gag(T559, T554, T552, T553, deleteD_out_gag(0, T554, T553)) → deleteD_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U25_gag(T425, T417, T420, T419, deleteD_out_gag(s(T425), T420, T419)) → deleteD_out_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419))
U22_gag(T377, T372, T370, T371, deleteD_out_gag(0, T372, T371)) → deleteD_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U10_ggag(T250, T251, T236, T235, deleteD_out_gag(s(T251), T236, T235)) → pG_out_ggag(T250, T251, T236, T235)
U18_gag(T251, T250, T233, T236, T235, pG_out_ggag(T250, T251, T236, T235)) → deleteD_out_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235))
U17_gag(T241, T233, T236, T235, deleteD_out_gag(s(T241), T236, T235)) → deleteD_out_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235))
U8_ggag(T198, T199, T182, T181, deleteD_out_gag(s(T198), T182, T181)) → pF_out_ggag(T198, T199, T182, T181)
U15_gag(T198, T199, T182, T180, T181, pF_out_ggag(T198, T199, T182, T181)) → deleteD_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U14_gag(T187, T182, T180, T181, deleteD_out_gag(0, T182, T181)) → deleteD_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, deleteD_out_gag(T158, T163, T162)) → pC_out_ggag(T159, T158, T163, T162)
U13_gag(T158, T159, T160, T163, T162, pC_out_ggag(T159, T158, T163, T162)) → deleteD_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, deleteD_out_gag(T121, T126, T125)) → pE_out_ggag(T121, T122, T126, T125)
U12_gag(T121, T122, T126, T124, T125, pE_out_ggag(T121, T122, T126, T125)) → deleteD_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
deleteD_in_gag(x1, x2, x3)  =  deleteD_in_gag(x1, x3)
deleteD_out_gag(x1, x2, x3)  =  deleteD_out_gag(x1, x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_gag(x1, x2, x3, x6, x7, x8, x9)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
delminA_out_agg(x1, x2, x3)  =  delminA_out_agg(x2, x3)
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x1, x4, x5, x6, x7)
U12_gag(x1, x2, x3, x4, x5, x6)  =  U12_gag(x1, x2, x4, x5, x6)
pE_in_ggag(x1, x2, x3, x4)  =  pE_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x2, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessB_out_gg(x1, x2)  =  lessB_out_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x1, x2, x3)
pE_out_ggag(x1, x2, x3, x4)  =  pE_out_ggag(x1, x2, x4)
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x1, x2, x4, x5)
U13_gag(x1, x2, x3, x4, x5, x6)  =  U13_gag(x1, x2, x3, x5, x6)
pC_in_ggag(x1, x2, x3, x4)  =  pC_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x1, x2, x4, x5)
pC_out_ggag(x1, x2, x3, x4)  =  pC_out_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x1, x2, x4, x5)
U14_gag(x1, x2, x3, x4, x5)  =  U14_gag(x1, x3, x4, x5)
U15_gag(x1, x2, x3, x4, x5, x6)  =  U15_gag(x1, x2, x4, x5, x6)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4, x5)  =  U7_ggag(x1, x2, x4, x5)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x4)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x1, x2, x4, x5)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x1, x2, x3, x5, x6)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x2, x4, x5)
U18_gag(x1, x2, x3, x4, x5, x6)  =  U18_gag(x1, x2, x3, x5, x6)
pG_in_ggag(x1, x2, x3, x4)  =  pG_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x2, x4, x5)
pG_out_ggag(x1, x2, x3, x4)  =  pG_out_ggag(x1, x2, x4)
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x1, x2, x4, x5)
U19_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_gag(x1, x2, x3, x6, x7, x8, x9)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x1, x2, x4, x5, x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x1, x2, x3, x5, x6)
U22_gag(x1, x2, x3, x4, x5)  =  U22_gag(x1, x3, x4, x5)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x1, x2, x4, x5, x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x1, x2, x3, x5, x6)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x1, x2, x4, x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x1, x2, x3, x5, x6)
U27_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_gag(x1, x2, x3, x6, x7, x8, x9)
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x1, x2, x4, x5, x6)
U29_gag(x1, x2, x3, x4, x5, x6)  =  U29_gag(x1, x2, x3, x5, x6)
U30_gag(x1, x2, x3, x4, x5)  =  U30_gag(x1, x3, x4, x5)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x1, x2, x4, x5, x6)
U32_gag(x1, x2, x3, x4, x5, x6)  =  U32_gag(x1, x2, x3, x5, x6)
U33_gag(x1, x2, x3, x4, x5)  =  U33_gag(x1, x2, x4, x5)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x1, x2, x3, x5, x6)
U35_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_gag(x1, x2, x3, x6, x7, x8, x9)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x1, x2, x4, x5, x6)
U37_gag(x1, x2, x3, x4, x5, x6)  =  U37_gag(x1, x2, x3, x5, x6)
U38_gag(x1, x2, x3, x4, x5)  =  U38_gag(x1, x3, x4, x5)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x1, x2, x4, x5, x6)
U40_gag(x1, x2, x3, x4, x5, x6)  =  U40_gag(x1, x2, x3, x5, x6)
U41_gag(x1, x2, x3, x4, x5)  =  U41_gag(x1, x2, x4, x5)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x1, x2, x3, x5, x6)
DELETED_IN_GAG(x1, x2, x3)  =  DELETED_IN_GAG(x1, x3)
U11_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_GAG(x1, x2, x3, x6, x7, x8, x9)
DELMINA_IN_AGG(x1, x2, x3)  =  DELMINA_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AGG(x1, x4, x5, x6, x7)
U12_GAG(x1, x2, x3, x4, x5, x6)  =  U12_GAG(x1, x2, x4, x5, x6)
PE_IN_GGAG(x1, x2, x3, x4)  =  PE_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x2, x4, x5)
LESSB_IN_GG(x1, x2)  =  LESSB_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U6_GGAG(x1, x2, x3, x4, x5)  =  U6_GGAG(x1, x2, x4, x5)
U13_GAG(x1, x2, x3, x4, x5, x6)  =  U13_GAG(x1, x2, x3, x5, x6)
PC_IN_GGAG(x1, x2, x3, x4)  =  PC_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5)  =  U3_GGAG(x1, x2, x4, x5)
U4_GGAG(x1, x2, x3, x4, x5)  =  U4_GGAG(x1, x2, x4, x5)
U14_GAG(x1, x2, x3, x4, x5)  =  U14_GAG(x1, x3, x4, x5)
U15_GAG(x1, x2, x3, x4, x5, x6)  =  U15_GAG(x1, x2, x4, x5, x6)
PF_IN_GGAG(x1, x2, x3, x4)  =  PF_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4, x5)  =  U7_GGAG(x1, x2, x4, x5)
U8_GGAG(x1, x2, x3, x4, x5)  =  U8_GGAG(x1, x2, x4, x5)
U16_GAG(x1, x2, x3, x4, x5, x6)  =  U16_GAG(x1, x2, x3, x5, x6)
U17_GAG(x1, x2, x3, x4, x5)  =  U17_GAG(x1, x2, x4, x5)
U18_GAG(x1, x2, x3, x4, x5, x6)  =  U18_GAG(x1, x2, x3, x5, x6)
PG_IN_GGAG(x1, x2, x3, x4)  =  PG_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x2, x4, x5)
U10_GGAG(x1, x2, x3, x4, x5)  =  U10_GGAG(x1, x2, x4, x5)
U19_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_GAG(x1, x2, x3, x6, x7, x8, x9)
U20_GAG(x1, x2, x3, x4, x5, x6)  =  U20_GAG(x1, x2, x4, x5, x6)
U21_GAG(x1, x2, x3, x4, x5, x6)  =  U21_GAG(x1, x2, x3, x5, x6)
U22_GAG(x1, x2, x3, x4, x5)  =  U22_GAG(x1, x3, x4, x5)
U23_GAG(x1, x2, x3, x4, x5, x6)  =  U23_GAG(x1, x2, x4, x5, x6)
U24_GAG(x1, x2, x3, x4, x5, x6)  =  U24_GAG(x1, x2, x3, x5, x6)
U25_GAG(x1, x2, x3, x4, x5)  =  U25_GAG(x1, x2, x4, x5)
U26_GAG(x1, x2, x3, x4, x5, x6)  =  U26_GAG(x1, x2, x3, x5, x6)
U27_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_GAG(x1, x2, x3, x6, x7, x8, x9)
U28_GAG(x1, x2, x3, x4, x5, x6)  =  U28_GAG(x1, x2, x4, x5, x6)
U29_GAG(x1, x2, x3, x4, x5, x6)  =  U29_GAG(x1, x2, x3, x5, x6)
U30_GAG(x1, x2, x3, x4, x5)  =  U30_GAG(x1, x3, x4, x5)
U31_GAG(x1, x2, x3, x4, x5, x6)  =  U31_GAG(x1, x2, x4, x5, x6)
U32_GAG(x1, x2, x3, x4, x5, x6)  =  U32_GAG(x1, x2, x3, x5, x6)
U33_GAG(x1, x2, x3, x4, x5)  =  U33_GAG(x1, x2, x4, x5)
U34_GAG(x1, x2, x3, x4, x5, x6)  =  U34_GAG(x1, x2, x3, x5, x6)
U35_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_GAG(x1, x2, x3, x6, x7, x8, x9)
U36_GAG(x1, x2, x3, x4, x5, x6)  =  U36_GAG(x1, x2, x4, x5, x6)
U37_GAG(x1, x2, x3, x4, x5, x6)  =  U37_GAG(x1, x2, x3, x5, x6)
U38_GAG(x1, x2, x3, x4, x5)  =  U38_GAG(x1, x3, x4, x5)
U39_GAG(x1, x2, x3, x4, x5, x6)  =  U39_GAG(x1, x2, x4, x5, x6)
U40_GAG(x1, x2, x3, x4, x5, x6)  =  U40_GAG(x1, x2, x3, x5, x6)
U41_GAG(x1, x2, x3, x4, x5)  =  U41_GAG(x1, x2, x4, x5)
U42_GAG(x1, x2, x3, x4, x5, x6)  =  U42_GAG(x1, x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 43 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSB_IN_GG(s(T140), s(T141)) → LESSB_IN_GG(T140, T141)

The TRS R consists of the following rules:

deleteD_in_gag(T6, tree(T6, void, T7), T7) → deleteD_out_gag(T6, tree(T6, void, T7), T7)
deleteD_in_gag(T10, tree(T10, T11, void), T11) → deleteD_out_gag(T10, tree(T10, T11, void), T11)
deleteD_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → deleteD_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
deleteD_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
delminA_in_agg(tree(T76, void, T77), T76, T77) → delminA_out_agg(tree(T76, void, T77), T76, T77)
delminA_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delminA_out_agg(T96, T93, T94)) → delminA_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_out_agg(T63, T60, T61)) → deleteD_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
deleteD_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_gag(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
pE_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, lessB_in_gg(T121, T122))
lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → pE_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
deleteD_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_gag(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
pC_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → pC_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
deleteD_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_gag(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
deleteD_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_gag(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
pF_in_ggag(T198, T199, T182, T181) → U7_ggag(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → pF_out_ggag(T198, T199, T182, T181)
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_ggag(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
deleteD_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_gag(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
U16_gag(T218, T219, T220, T223, T222, pC_out_ggag(T219, T218, T223, T222)) → deleteD_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
deleteD_in_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_gag(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
deleteD_in_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_gag(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
pG_in_ggag(T250, T251, T236, T235) → U9_ggag(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → pG_out_ggag(T250, T251, T236, T235)
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_ggag(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
deleteD_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_out_agg(T311, T308, T309)) → deleteD_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
deleteD_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_gag(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
U20_gag(T336, T337, T341, T339, T340, pE_out_ggag(T336, T337, T341, T340)) → deleteD_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
deleteD_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_gag(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
U21_gag(T354, T355, T356, T359, T358, pC_out_ggag(T355, T354, T359, T358)) → deleteD_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
deleteD_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_gag(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
deleteD_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_gag(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
U23_gag(T388, T389, T372, T370, T371, pF_out_ggag(T388, T389, T372, T371)) → deleteD_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
deleteD_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_gag(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
U24_gag(T402, T403, T404, T407, T406, pC_out_ggag(T403, T402, T407, T406)) → deleteD_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
deleteD_in_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_gag(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
deleteD_in_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_gag(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
U26_gag(T435, T434, T417, T420, T419, pG_out_ggag(T434, T435, T420, T419)) → deleteD_out_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419))
deleteD_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_out_agg(T493, T490, T491)) → deleteD_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
deleteD_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_gag(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
U28_gag(T518, T519, T523, T521, T522, pE_out_ggag(T518, T519, T523, T522)) → deleteD_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
deleteD_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_gag(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
U29_gag(T536, T537, T538, T541, T540, pC_out_ggag(T537, T536, T541, T540)) → deleteD_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
deleteD_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_gag(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
deleteD_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_gag(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
U31_gag(T570, T571, T554, T552, T553, pF_out_ggag(T570, T571, T554, T553)) → deleteD_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
deleteD_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_gag(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
U32_gag(T584, T585, T586, T589, T588, pC_out_ggag(T585, T584, T589, T588)) → deleteD_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
deleteD_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_gag(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
deleteD_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_gag(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
U34_gag(T617, T616, T599, T602, T601, pG_out_ggag(T616, T617, T602, T601)) → deleteD_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
deleteD_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_out_agg(T671, T668, T669)) → deleteD_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
deleteD_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_gag(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
U36_gag(T696, T697, T701, T699, T700, pE_out_ggag(T696, T697, T701, T700)) → deleteD_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
deleteD_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_gag(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
U37_gag(T714, T715, T716, T719, T718, pC_out_ggag(T715, T714, T719, T718)) → deleteD_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
deleteD_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_gag(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
deleteD_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_gag(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
U39_gag(T748, T749, T732, T730, T731, pF_out_ggag(T748, T749, T732, T731)) → deleteD_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
deleteD_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_gag(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
U40_gag(T762, T763, T764, T767, T766, pC_out_ggag(T763, T762, T767, T766)) → deleteD_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
deleteD_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_gag(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
deleteD_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_gag(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))
U42_gag(T795, T794, T777, T780, T779, pG_out_ggag(T794, T795, T780, T779)) → deleteD_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U41_gag(T785, T777, T780, T779, deleteD_out_gag(s(T785), T780, T779)) → deleteD_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U38_gag(T737, T732, T730, T731, deleteD_out_gag(0, T732, T731)) → deleteD_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U33_gag(T607, T599, T602, T601, deleteD_out_gag(s(T607), T602, T601)) → deleteD_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U30_gag(T559, T554, T552, T553, deleteD_out_gag(0, T554, T553)) → deleteD_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U25_gag(T425, T417, T420, T419, deleteD_out_gag(s(T425), T420, T419)) → deleteD_out_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419))
U22_gag(T377, T372, T370, T371, deleteD_out_gag(0, T372, T371)) → deleteD_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U10_ggag(T250, T251, T236, T235, deleteD_out_gag(s(T251), T236, T235)) → pG_out_ggag(T250, T251, T236, T235)
U18_gag(T251, T250, T233, T236, T235, pG_out_ggag(T250, T251, T236, T235)) → deleteD_out_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235))
U17_gag(T241, T233, T236, T235, deleteD_out_gag(s(T241), T236, T235)) → deleteD_out_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235))
U8_ggag(T198, T199, T182, T181, deleteD_out_gag(s(T198), T182, T181)) → pF_out_ggag(T198, T199, T182, T181)
U15_gag(T198, T199, T182, T180, T181, pF_out_ggag(T198, T199, T182, T181)) → deleteD_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U14_gag(T187, T182, T180, T181, deleteD_out_gag(0, T182, T181)) → deleteD_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, deleteD_out_gag(T158, T163, T162)) → pC_out_ggag(T159, T158, T163, T162)
U13_gag(T158, T159, T160, T163, T162, pC_out_ggag(T159, T158, T163, T162)) → deleteD_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, deleteD_out_gag(T121, T126, T125)) → pE_out_ggag(T121, T122, T126, T125)
U12_gag(T121, T122, T126, T124, T125, pE_out_ggag(T121, T122, T126, T125)) → deleteD_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
deleteD_in_gag(x1, x2, x3)  =  deleteD_in_gag(x1, x3)
deleteD_out_gag(x1, x2, x3)  =  deleteD_out_gag(x1, x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_gag(x1, x2, x3, x6, x7, x8, x9)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
delminA_out_agg(x1, x2, x3)  =  delminA_out_agg(x2, x3)
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x1, x4, x5, x6, x7)
U12_gag(x1, x2, x3, x4, x5, x6)  =  U12_gag(x1, x2, x4, x5, x6)
pE_in_ggag(x1, x2, x3, x4)  =  pE_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x2, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessB_out_gg(x1, x2)  =  lessB_out_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x1, x2, x3)
pE_out_ggag(x1, x2, x3, x4)  =  pE_out_ggag(x1, x2, x4)
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x1, x2, x4, x5)
U13_gag(x1, x2, x3, x4, x5, x6)  =  U13_gag(x1, x2, x3, x5, x6)
pC_in_ggag(x1, x2, x3, x4)  =  pC_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x1, x2, x4, x5)
pC_out_ggag(x1, x2, x3, x4)  =  pC_out_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x1, x2, x4, x5)
U14_gag(x1, x2, x3, x4, x5)  =  U14_gag(x1, x3, x4, x5)
U15_gag(x1, x2, x3, x4, x5, x6)  =  U15_gag(x1, x2, x4, x5, x6)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4, x5)  =  U7_ggag(x1, x2, x4, x5)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x4)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x1, x2, x4, x5)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x1, x2, x3, x5, x6)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x2, x4, x5)
U18_gag(x1, x2, x3, x4, x5, x6)  =  U18_gag(x1, x2, x3, x5, x6)
pG_in_ggag(x1, x2, x3, x4)  =  pG_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x2, x4, x5)
pG_out_ggag(x1, x2, x3, x4)  =  pG_out_ggag(x1, x2, x4)
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x1, x2, x4, x5)
U19_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_gag(x1, x2, x3, x6, x7, x8, x9)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x1, x2, x4, x5, x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x1, x2, x3, x5, x6)
U22_gag(x1, x2, x3, x4, x5)  =  U22_gag(x1, x3, x4, x5)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x1, x2, x4, x5, x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x1, x2, x3, x5, x6)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x1, x2, x4, x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x1, x2, x3, x5, x6)
U27_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_gag(x1, x2, x3, x6, x7, x8, x9)
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x1, x2, x4, x5, x6)
U29_gag(x1, x2, x3, x4, x5, x6)  =  U29_gag(x1, x2, x3, x5, x6)
U30_gag(x1, x2, x3, x4, x5)  =  U30_gag(x1, x3, x4, x5)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x1, x2, x4, x5, x6)
U32_gag(x1, x2, x3, x4, x5, x6)  =  U32_gag(x1, x2, x3, x5, x6)
U33_gag(x1, x2, x3, x4, x5)  =  U33_gag(x1, x2, x4, x5)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x1, x2, x3, x5, x6)
U35_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_gag(x1, x2, x3, x6, x7, x8, x9)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x1, x2, x4, x5, x6)
U37_gag(x1, x2, x3, x4, x5, x6)  =  U37_gag(x1, x2, x3, x5, x6)
U38_gag(x1, x2, x3, x4, x5)  =  U38_gag(x1, x3, x4, x5)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x1, x2, x4, x5, x6)
U40_gag(x1, x2, x3, x4, x5, x6)  =  U40_gag(x1, x2, x3, x5, x6)
U41_gag(x1, x2, x3, x4, x5)  =  U41_gag(x1, x2, x4, x5)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x1, x2, x3, x5, x6)
LESSB_IN_GG(x1, x2)  =  LESSB_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSB_IN_GG(s(T140), s(T141)) → LESSB_IN_GG(T140, T141)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSB_IN_GG(s(T140), s(T141)) → LESSB_IN_GG(T140, T141)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSB_IN_GG(s(T140), s(T141)) → LESSB_IN_GG(T140, T141)
    The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMINA_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMINA_IN_AGG(T96, T93, T94)

The TRS R consists of the following rules:

deleteD_in_gag(T6, tree(T6, void, T7), T7) → deleteD_out_gag(T6, tree(T6, void, T7), T7)
deleteD_in_gag(T10, tree(T10, T11, void), T11) → deleteD_out_gag(T10, tree(T10, T11, void), T11)
deleteD_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → deleteD_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
deleteD_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
delminA_in_agg(tree(T76, void, T77), T76, T77) → delminA_out_agg(tree(T76, void, T77), T76, T77)
delminA_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delminA_out_agg(T96, T93, T94)) → delminA_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_out_agg(T63, T60, T61)) → deleteD_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
deleteD_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_gag(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
pE_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, lessB_in_gg(T121, T122))
lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → pE_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
deleteD_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_gag(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
pC_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → pC_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
deleteD_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_gag(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
deleteD_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_gag(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
pF_in_ggag(T198, T199, T182, T181) → U7_ggag(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → pF_out_ggag(T198, T199, T182, T181)
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_ggag(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
deleteD_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_gag(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
U16_gag(T218, T219, T220, T223, T222, pC_out_ggag(T219, T218, T223, T222)) → deleteD_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
deleteD_in_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_gag(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
deleteD_in_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_gag(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
pG_in_ggag(T250, T251, T236, T235) → U9_ggag(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → pG_out_ggag(T250, T251, T236, T235)
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_ggag(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
deleteD_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_out_agg(T311, T308, T309)) → deleteD_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
deleteD_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_gag(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
U20_gag(T336, T337, T341, T339, T340, pE_out_ggag(T336, T337, T341, T340)) → deleteD_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
deleteD_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_gag(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
U21_gag(T354, T355, T356, T359, T358, pC_out_ggag(T355, T354, T359, T358)) → deleteD_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
deleteD_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_gag(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
deleteD_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_gag(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
U23_gag(T388, T389, T372, T370, T371, pF_out_ggag(T388, T389, T372, T371)) → deleteD_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
deleteD_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_gag(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
U24_gag(T402, T403, T404, T407, T406, pC_out_ggag(T403, T402, T407, T406)) → deleteD_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
deleteD_in_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_gag(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
deleteD_in_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_gag(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
U26_gag(T435, T434, T417, T420, T419, pG_out_ggag(T434, T435, T420, T419)) → deleteD_out_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419))
deleteD_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_out_agg(T493, T490, T491)) → deleteD_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
deleteD_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_gag(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
U28_gag(T518, T519, T523, T521, T522, pE_out_ggag(T518, T519, T523, T522)) → deleteD_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
deleteD_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_gag(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
U29_gag(T536, T537, T538, T541, T540, pC_out_ggag(T537, T536, T541, T540)) → deleteD_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
deleteD_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_gag(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
deleteD_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_gag(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
U31_gag(T570, T571, T554, T552, T553, pF_out_ggag(T570, T571, T554, T553)) → deleteD_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
deleteD_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_gag(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
U32_gag(T584, T585, T586, T589, T588, pC_out_ggag(T585, T584, T589, T588)) → deleteD_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
deleteD_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_gag(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
deleteD_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_gag(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
U34_gag(T617, T616, T599, T602, T601, pG_out_ggag(T616, T617, T602, T601)) → deleteD_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
deleteD_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_out_agg(T671, T668, T669)) → deleteD_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
deleteD_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_gag(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
U36_gag(T696, T697, T701, T699, T700, pE_out_ggag(T696, T697, T701, T700)) → deleteD_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
deleteD_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_gag(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
U37_gag(T714, T715, T716, T719, T718, pC_out_ggag(T715, T714, T719, T718)) → deleteD_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
deleteD_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_gag(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
deleteD_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_gag(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
U39_gag(T748, T749, T732, T730, T731, pF_out_ggag(T748, T749, T732, T731)) → deleteD_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
deleteD_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_gag(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
U40_gag(T762, T763, T764, T767, T766, pC_out_ggag(T763, T762, T767, T766)) → deleteD_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
deleteD_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_gag(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
deleteD_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_gag(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))
U42_gag(T795, T794, T777, T780, T779, pG_out_ggag(T794, T795, T780, T779)) → deleteD_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U41_gag(T785, T777, T780, T779, deleteD_out_gag(s(T785), T780, T779)) → deleteD_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U38_gag(T737, T732, T730, T731, deleteD_out_gag(0, T732, T731)) → deleteD_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U33_gag(T607, T599, T602, T601, deleteD_out_gag(s(T607), T602, T601)) → deleteD_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U30_gag(T559, T554, T552, T553, deleteD_out_gag(0, T554, T553)) → deleteD_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U25_gag(T425, T417, T420, T419, deleteD_out_gag(s(T425), T420, T419)) → deleteD_out_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419))
U22_gag(T377, T372, T370, T371, deleteD_out_gag(0, T372, T371)) → deleteD_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U10_ggag(T250, T251, T236, T235, deleteD_out_gag(s(T251), T236, T235)) → pG_out_ggag(T250, T251, T236, T235)
U18_gag(T251, T250, T233, T236, T235, pG_out_ggag(T250, T251, T236, T235)) → deleteD_out_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235))
U17_gag(T241, T233, T236, T235, deleteD_out_gag(s(T241), T236, T235)) → deleteD_out_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235))
U8_ggag(T198, T199, T182, T181, deleteD_out_gag(s(T198), T182, T181)) → pF_out_ggag(T198, T199, T182, T181)
U15_gag(T198, T199, T182, T180, T181, pF_out_ggag(T198, T199, T182, T181)) → deleteD_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U14_gag(T187, T182, T180, T181, deleteD_out_gag(0, T182, T181)) → deleteD_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, deleteD_out_gag(T158, T163, T162)) → pC_out_ggag(T159, T158, T163, T162)
U13_gag(T158, T159, T160, T163, T162, pC_out_ggag(T159, T158, T163, T162)) → deleteD_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, deleteD_out_gag(T121, T126, T125)) → pE_out_ggag(T121, T122, T126, T125)
U12_gag(T121, T122, T126, T124, T125, pE_out_ggag(T121, T122, T126, T125)) → deleteD_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
deleteD_in_gag(x1, x2, x3)  =  deleteD_in_gag(x1, x3)
deleteD_out_gag(x1, x2, x3)  =  deleteD_out_gag(x1, x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_gag(x1, x2, x3, x6, x7, x8, x9)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
delminA_out_agg(x1, x2, x3)  =  delminA_out_agg(x2, x3)
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x1, x4, x5, x6, x7)
U12_gag(x1, x2, x3, x4, x5, x6)  =  U12_gag(x1, x2, x4, x5, x6)
pE_in_ggag(x1, x2, x3, x4)  =  pE_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x2, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessB_out_gg(x1, x2)  =  lessB_out_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x1, x2, x3)
pE_out_ggag(x1, x2, x3, x4)  =  pE_out_ggag(x1, x2, x4)
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x1, x2, x4, x5)
U13_gag(x1, x2, x3, x4, x5, x6)  =  U13_gag(x1, x2, x3, x5, x6)
pC_in_ggag(x1, x2, x3, x4)  =  pC_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x1, x2, x4, x5)
pC_out_ggag(x1, x2, x3, x4)  =  pC_out_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x1, x2, x4, x5)
U14_gag(x1, x2, x3, x4, x5)  =  U14_gag(x1, x3, x4, x5)
U15_gag(x1, x2, x3, x4, x5, x6)  =  U15_gag(x1, x2, x4, x5, x6)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4, x5)  =  U7_ggag(x1, x2, x4, x5)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x4)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x1, x2, x4, x5)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x1, x2, x3, x5, x6)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x2, x4, x5)
U18_gag(x1, x2, x3, x4, x5, x6)  =  U18_gag(x1, x2, x3, x5, x6)
pG_in_ggag(x1, x2, x3, x4)  =  pG_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x2, x4, x5)
pG_out_ggag(x1, x2, x3, x4)  =  pG_out_ggag(x1, x2, x4)
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x1, x2, x4, x5)
U19_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_gag(x1, x2, x3, x6, x7, x8, x9)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x1, x2, x4, x5, x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x1, x2, x3, x5, x6)
U22_gag(x1, x2, x3, x4, x5)  =  U22_gag(x1, x3, x4, x5)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x1, x2, x4, x5, x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x1, x2, x3, x5, x6)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x1, x2, x4, x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x1, x2, x3, x5, x6)
U27_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_gag(x1, x2, x3, x6, x7, x8, x9)
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x1, x2, x4, x5, x6)
U29_gag(x1, x2, x3, x4, x5, x6)  =  U29_gag(x1, x2, x3, x5, x6)
U30_gag(x1, x2, x3, x4, x5)  =  U30_gag(x1, x3, x4, x5)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x1, x2, x4, x5, x6)
U32_gag(x1, x2, x3, x4, x5, x6)  =  U32_gag(x1, x2, x3, x5, x6)
U33_gag(x1, x2, x3, x4, x5)  =  U33_gag(x1, x2, x4, x5)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x1, x2, x3, x5, x6)
U35_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_gag(x1, x2, x3, x6, x7, x8, x9)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x1, x2, x4, x5, x6)
U37_gag(x1, x2, x3, x4, x5, x6)  =  U37_gag(x1, x2, x3, x5, x6)
U38_gag(x1, x2, x3, x4, x5)  =  U38_gag(x1, x3, x4, x5)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x1, x2, x4, x5, x6)
U40_gag(x1, x2, x3, x4, x5, x6)  =  U40_gag(x1, x2, x3, x5, x6)
U41_gag(x1, x2, x3, x4, x5)  =  U41_gag(x1, x2, x4, x5)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x1, x2, x3, x5, x6)
DELMINA_IN_AGG(x1, x2, x3)  =  DELMINA_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMINA_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMINA_IN_AGG(T96, T93, T94)

R is empty.
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
DELMINA_IN_AGG(x1, x2, x3)  =  DELMINA_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELMINA_IN_AGG(T93, tree(T90, T94, T95)) → DELMINA_IN_AGG(T93, T94)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELMINA_IN_AGG(T93, tree(T90, T94, T95)) → DELMINA_IN_AGG(T93, T94)
    The graph contains the following edges 1 >= 1, 2 > 2

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETED_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → PE_IN_GGAG(T121, T122, T126, T125)
PE_IN_GGAG(T121, T122, T126, T125) → U5_GGAG(T121, T122, T126, T125, lessB_in_gg(T121, T122))
U5_GGAG(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → DELETED_IN_GAG(T121, T126, T125)
DELETED_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → PC_IN_GGAG(T159, T158, T163, T162)
PC_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_GGAG(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → DELETED_IN_GAG(T158, T163, T162)
DELETED_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETED_IN_GAG(0, T182, T181)
DELETED_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → PF_IN_GGAG(T198, T199, T182, T181)
PF_IN_GGAG(T198, T199, T182, T181) → U7_GGAG(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_GGAG(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → DELETED_IN_GAG(s(T198), T182, T181)
DELETED_IN_GAG(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → DELETED_IN_GAG(s(T241), T236, T235)
DELETED_IN_GAG(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → PG_IN_GGAG(T250, T251, T236, T235)
PG_IN_GGAG(T250, T251, T236, T235) → U9_GGAG(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_GGAG(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → DELETED_IN_GAG(s(T251), T236, T235)

The TRS R consists of the following rules:

deleteD_in_gag(T6, tree(T6, void, T7), T7) → deleteD_out_gag(T6, tree(T6, void, T7), T7)
deleteD_in_gag(T10, tree(T10, T11, void), T11) → deleteD_out_gag(T10, tree(T10, T11, void), T11)
deleteD_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → deleteD_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
deleteD_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_in_agg(T63, T60, T61))
delminA_in_agg(tree(T76, void, T77), T76, T77) → delminA_out_agg(tree(T76, void, T77), T76, T77)
delminA_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delminA_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delminA_out_agg(T96, T93, T94)) → delminA_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U11_gag(T17, T18, T57, T63, T59, T60, T61, T62, delminA_out_agg(T63, T60, T61)) → deleteD_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
deleteD_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U12_gag(T121, T122, T126, T124, T125, pE_in_ggag(T121, T122, T126, T125))
pE_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, lessB_in_gg(T121, T122))
lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → pE_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, deleteD_in_gag(T121, T126, T125))
deleteD_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U13_gag(T158, T159, T160, T163, T162, pC_in_ggag(T159, T158, T163, T162))
pC_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → pC_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, deleteD_in_gag(T158, T163, T162))
deleteD_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U14_gag(T187, T182, T180, T181, deleteD_in_gag(0, T182, T181))
deleteD_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U15_gag(T198, T199, T182, T180, T181, pF_in_ggag(T198, T199, T182, T181))
pF_in_ggag(T198, T199, T182, T181) → U7_ggag(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → pF_out_ggag(T198, T199, T182, T181)
U7_ggag(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → U8_ggag(T198, T199, T182, T181, deleteD_in_gag(s(T198), T182, T181))
deleteD_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U16_gag(T218, T219, T220, T223, T222, pC_in_ggag(T219, T218, T223, T222))
U16_gag(T218, T219, T220, T223, T222, pC_out_ggag(T219, T218, T223, T222)) → deleteD_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
deleteD_in_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → U17_gag(T241, T233, T236, T235, deleteD_in_gag(s(T241), T236, T235))
deleteD_in_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → U18_gag(T251, T250, T233, T236, T235, pG_in_ggag(T250, T251, T236, T235))
pG_in_ggag(T250, T251, T236, T235) → U9_ggag(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → pG_out_ggag(T250, T251, T236, T235)
U9_ggag(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → U10_ggag(T250, T251, T236, T235, deleteD_in_gag(s(T251), T236, T235))
deleteD_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_in_agg(T311, T308, T309))
U19_gag(T265, T266, T305, T311, T307, T308, T309, T310, delminA_out_agg(T311, T308, T309)) → deleteD_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
deleteD_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U20_gag(T336, T337, T341, T339, T340, pE_in_ggag(T336, T337, T341, T340))
U20_gag(T336, T337, T341, T339, T340, pE_out_ggag(T336, T337, T341, T340)) → deleteD_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
deleteD_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U21_gag(T354, T355, T356, T359, T358, pC_in_ggag(T355, T354, T359, T358))
U21_gag(T354, T355, T356, T359, T358, pC_out_ggag(T355, T354, T359, T358)) → deleteD_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
deleteD_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U22_gag(T377, T372, T370, T371, deleteD_in_gag(0, T372, T371))
deleteD_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U23_gag(T388, T389, T372, T370, T371, pF_in_ggag(T388, T389, T372, T371))
U23_gag(T388, T389, T372, T370, T371, pF_out_ggag(T388, T389, T372, T371)) → deleteD_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
deleteD_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U24_gag(T402, T403, T404, T407, T406, pC_in_ggag(T403, T402, T407, T406))
U24_gag(T402, T403, T404, T407, T406, pC_out_ggag(T403, T402, T407, T406)) → deleteD_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
deleteD_in_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419)) → U25_gag(T425, T417, T420, T419, deleteD_in_gag(s(T425), T420, T419))
deleteD_in_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419)) → U26_gag(T435, T434, T417, T420, T419, pG_in_ggag(T434, T435, T420, T419))
U26_gag(T435, T434, T417, T420, T419, pG_out_ggag(T434, T435, T420, T419)) → deleteD_out_gag(s(T435), tree(s(T434), T417, T420), tree(s(T434), T417, T419))
deleteD_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_in_agg(T493, T490, T491))
U27_gag(T447, T448, T487, T493, T489, T490, T491, T492, delminA_out_agg(T493, T490, T491)) → deleteD_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
deleteD_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U28_gag(T518, T519, T523, T521, T522, pE_in_ggag(T518, T519, T523, T522))
U28_gag(T518, T519, T523, T521, T522, pE_out_ggag(T518, T519, T523, T522)) → deleteD_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
deleteD_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U29_gag(T536, T537, T538, T541, T540, pC_in_ggag(T537, T536, T541, T540))
U29_gag(T536, T537, T538, T541, T540, pC_out_ggag(T537, T536, T541, T540)) → deleteD_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
deleteD_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U30_gag(T559, T554, T552, T553, deleteD_in_gag(0, T554, T553))
deleteD_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U31_gag(T570, T571, T554, T552, T553, pF_in_ggag(T570, T571, T554, T553))
U31_gag(T570, T571, T554, T552, T553, pF_out_ggag(T570, T571, T554, T553)) → deleteD_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
deleteD_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U32_gag(T584, T585, T586, T589, T588, pC_in_ggag(T585, T584, T589, T588))
U32_gag(T584, T585, T586, T589, T588, pC_out_ggag(T585, T584, T589, T588)) → deleteD_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
deleteD_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U33_gag(T607, T599, T602, T601, deleteD_in_gag(s(T607), T602, T601))
deleteD_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U34_gag(T617, T616, T599, T602, T601, pG_in_ggag(T616, T617, T602, T601))
U34_gag(T617, T616, T599, T602, T601, pG_out_ggag(T616, T617, T602, T601)) → deleteD_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
deleteD_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_in_agg(T671, T668, T669))
U35_gag(T625, T626, T665, T671, T667, T668, T669, T670, delminA_out_agg(T671, T668, T669)) → deleteD_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
deleteD_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U36_gag(T696, T697, T701, T699, T700, pE_in_ggag(T696, T697, T701, T700))
U36_gag(T696, T697, T701, T699, T700, pE_out_ggag(T696, T697, T701, T700)) → deleteD_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
deleteD_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U37_gag(T714, T715, T716, T719, T718, pC_in_ggag(T715, T714, T719, T718))
U37_gag(T714, T715, T716, T719, T718, pC_out_ggag(T715, T714, T719, T718)) → deleteD_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
deleteD_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U38_gag(T737, T732, T730, T731, deleteD_in_gag(0, T732, T731))
deleteD_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U39_gag(T748, T749, T732, T730, T731, pF_in_ggag(T748, T749, T732, T731))
U39_gag(T748, T749, T732, T730, T731, pF_out_ggag(T748, T749, T732, T731)) → deleteD_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
deleteD_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U40_gag(T762, T763, T764, T767, T766, pC_in_ggag(T763, T762, T767, T766))
U40_gag(T762, T763, T764, T767, T766, pC_out_ggag(T763, T762, T767, T766)) → deleteD_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
deleteD_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U41_gag(T785, T777, T780, T779, deleteD_in_gag(s(T785), T780, T779))
deleteD_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U42_gag(T795, T794, T777, T780, T779, pG_in_ggag(T794, T795, T780, T779))
U42_gag(T795, T794, T777, T780, T779, pG_out_ggag(T794, T795, T780, T779)) → deleteD_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U41_gag(T785, T777, T780, T779, deleteD_out_gag(s(T785), T780, T779)) → deleteD_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U38_gag(T737, T732, T730, T731, deleteD_out_gag(0, T732, T731)) → deleteD_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U33_gag(T607, T599, T602, T601, deleteD_out_gag(s(T607), T602, T601)) → deleteD_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U30_gag(T559, T554, T552, T553, deleteD_out_gag(0, T554, T553)) → deleteD_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U25_gag(T425, T417, T420, T419, deleteD_out_gag(s(T425), T420, T419)) → deleteD_out_gag(s(T425), tree(0, T417, T420), tree(0, T417, T419))
U22_gag(T377, T372, T370, T371, deleteD_out_gag(0, T372, T371)) → deleteD_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U10_ggag(T250, T251, T236, T235, deleteD_out_gag(s(T251), T236, T235)) → pG_out_ggag(T250, T251, T236, T235)
U18_gag(T251, T250, T233, T236, T235, pG_out_ggag(T250, T251, T236, T235)) → deleteD_out_gag(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235))
U17_gag(T241, T233, T236, T235, deleteD_out_gag(s(T241), T236, T235)) → deleteD_out_gag(s(T241), tree(0, T233, T236), tree(0, T233, T235))
U8_ggag(T198, T199, T182, T181, deleteD_out_gag(s(T198), T182, T181)) → pF_out_ggag(T198, T199, T182, T181)
U15_gag(T198, T199, T182, T180, T181, pF_out_ggag(T198, T199, T182, T181)) → deleteD_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U14_gag(T187, T182, T180, T181, deleteD_out_gag(0, T182, T181)) → deleteD_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, deleteD_out_gag(T158, T163, T162)) → pC_out_ggag(T159, T158, T163, T162)
U13_gag(T158, T159, T160, T163, T162, pC_out_ggag(T159, T158, T163, T162)) → deleteD_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, deleteD_out_gag(T121, T126, T125)) → pE_out_ggag(T121, T122, T126, T125)
U12_gag(T121, T122, T126, T124, T125, pE_out_ggag(T121, T122, T126, T125)) → deleteD_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
deleteD_in_gag(x1, x2, x3)  =  deleteD_in_gag(x1, x3)
deleteD_out_gag(x1, x2, x3)  =  deleteD_out_gag(x1, x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U11_gag(x1, x2, x3, x6, x7, x8, x9)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
delminA_out_agg(x1, x2, x3)  =  delminA_out_agg(x2, x3)
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x1, x4, x5, x6, x7)
U12_gag(x1, x2, x3, x4, x5, x6)  =  U12_gag(x1, x2, x4, x5, x6)
pE_in_ggag(x1, x2, x3, x4)  =  pE_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x2, x4, x5)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessB_out_gg(x1, x2)  =  lessB_out_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x1, x2, x3)
pE_out_ggag(x1, x2, x3, x4)  =  pE_out_ggag(x1, x2, x4)
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x1, x2, x4, x5)
U13_gag(x1, x2, x3, x4, x5, x6)  =  U13_gag(x1, x2, x3, x5, x6)
pC_in_ggag(x1, x2, x3, x4)  =  pC_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x1, x2, x4, x5)
pC_out_ggag(x1, x2, x3, x4)  =  pC_out_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x1, x2, x4, x5)
U14_gag(x1, x2, x3, x4, x5)  =  U14_gag(x1, x3, x4, x5)
U15_gag(x1, x2, x3, x4, x5, x6)  =  U15_gag(x1, x2, x4, x5, x6)
pF_in_ggag(x1, x2, x3, x4)  =  pF_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4, x5)  =  U7_ggag(x1, x2, x4, x5)
pF_out_ggag(x1, x2, x3, x4)  =  pF_out_ggag(x1, x2, x4)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x1, x2, x4, x5)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x1, x2, x3, x5, x6)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x2, x4, x5)
U18_gag(x1, x2, x3, x4, x5, x6)  =  U18_gag(x1, x2, x3, x5, x6)
pG_in_ggag(x1, x2, x3, x4)  =  pG_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x2, x4, x5)
pG_out_ggag(x1, x2, x3, x4)  =  pG_out_ggag(x1, x2, x4)
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x1, x2, x4, x5)
U19_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U19_gag(x1, x2, x3, x6, x7, x8, x9)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x1, x2, x4, x5, x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x1, x2, x3, x5, x6)
U22_gag(x1, x2, x3, x4, x5)  =  U22_gag(x1, x3, x4, x5)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x1, x2, x4, x5, x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x1, x2, x3, x5, x6)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x1, x2, x4, x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x1, x2, x3, x5, x6)
U27_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_gag(x1, x2, x3, x6, x7, x8, x9)
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x1, x2, x4, x5, x6)
U29_gag(x1, x2, x3, x4, x5, x6)  =  U29_gag(x1, x2, x3, x5, x6)
U30_gag(x1, x2, x3, x4, x5)  =  U30_gag(x1, x3, x4, x5)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x1, x2, x4, x5, x6)
U32_gag(x1, x2, x3, x4, x5, x6)  =  U32_gag(x1, x2, x3, x5, x6)
U33_gag(x1, x2, x3, x4, x5)  =  U33_gag(x1, x2, x4, x5)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x1, x2, x3, x5, x6)
U35_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U35_gag(x1, x2, x3, x6, x7, x8, x9)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x1, x2, x4, x5, x6)
U37_gag(x1, x2, x3, x4, x5, x6)  =  U37_gag(x1, x2, x3, x5, x6)
U38_gag(x1, x2, x3, x4, x5)  =  U38_gag(x1, x3, x4, x5)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x1, x2, x4, x5, x6)
U40_gag(x1, x2, x3, x4, x5, x6)  =  U40_gag(x1, x2, x3, x5, x6)
U41_gag(x1, x2, x3, x4, x5)  =  U41_gag(x1, x2, x4, x5)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x1, x2, x3, x5, x6)
DELETED_IN_GAG(x1, x2, x3)  =  DELETED_IN_GAG(x1, x3)
PE_IN_GGAG(x1, x2, x3, x4)  =  PE_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x2, x4, x5)
PC_IN_GGAG(x1, x2, x3, x4)  =  PC_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5)  =  U3_GGAG(x1, x2, x4, x5)
PF_IN_GGAG(x1, x2, x3, x4)  =  PF_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4, x5)  =  U7_GGAG(x1, x2, x4, x5)
PG_IN_GGAG(x1, x2, x3, x4)  =  PG_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETED_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → PE_IN_GGAG(T121, T122, T126, T125)
PE_IN_GGAG(T121, T122, T126, T125) → U5_GGAG(T121, T122, T126, T125, lessB_in_gg(T121, T122))
U5_GGAG(T121, T122, T126, T125, lessB_out_gg(T121, T122)) → DELETED_IN_GAG(T121, T126, T125)
DELETED_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → PC_IN_GGAG(T159, T158, T163, T162)
PC_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, lessB_in_gg(T159, T158))
U3_GGAG(T159, T158, T163, T162, lessB_out_gg(T159, T158)) → DELETED_IN_GAG(T158, T163, T162)
DELETED_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETED_IN_GAG(0, T182, T181)
DELETED_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → PF_IN_GGAG(T198, T199, T182, T181)
PF_IN_GGAG(T198, T199, T182, T181) → U7_GGAG(T198, T199, T182, T181, lessB_in_gg(T198, T199))
U7_GGAG(T198, T199, T182, T181, lessB_out_gg(T198, T199)) → DELETED_IN_GAG(s(T198), T182, T181)
DELETED_IN_GAG(s(T241), tree(0, T233, T236), tree(0, T233, T235)) → DELETED_IN_GAG(s(T241), T236, T235)
DELETED_IN_GAG(s(T251), tree(s(T250), T233, T236), tree(s(T250), T233, T235)) → PG_IN_GGAG(T250, T251, T236, T235)
PG_IN_GGAG(T250, T251, T236, T235) → U9_GGAG(T250, T251, T236, T235, lessB_in_gg(T250, T251))
U9_GGAG(T250, T251, T236, T235, lessB_out_gg(T250, T251)) → DELETED_IN_GAG(s(T251), T236, T235)

The TRS R consists of the following rules:

lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
lessB_in_gg(x1, x2)  =  lessB_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
lessB_out_gg(x1, x2)  =  lessB_out_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x1, x2, x3)
DELETED_IN_GAG(x1, x2, x3)  =  DELETED_IN_GAG(x1, x3)
PE_IN_GGAG(x1, x2, x3, x4)  =  PE_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x2, x4, x5)
PC_IN_GGAG(x1, x2, x3, x4)  =  PC_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5)  =  U3_GGAG(x1, x2, x4, x5)
PF_IN_GGAG(x1, x2, x3, x4)  =  PF_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4, x5)  =  U7_GGAG(x1, x2, x4, x5)
PG_IN_GGAG(x1, x2, x3, x4)  =  PG_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETED_IN_GAG(T121, tree(T122, T125, T124)) → PE_IN_GGAG(T121, T122, T125)
PE_IN_GGAG(T121, T122, T125) → U5_GGAG(T121, T122, T125, lessB_in_gg(T121, T122))
U5_GGAG(T121, T122, T125, lessB_out_gg(T121, T122)) → DELETED_IN_GAG(T121, T125)
DELETED_IN_GAG(T158, tree(T159, T160, T162)) → PC_IN_GGAG(T159, T158, T162)
PC_IN_GGAG(T159, T158, T162) → U3_GGAG(T159, T158, T162, lessB_in_gg(T159, T158))
U3_GGAG(T159, T158, T162, lessB_out_gg(T159, T158)) → DELETED_IN_GAG(T158, T162)
DELETED_IN_GAG(0, tree(s(T187), T181, T180)) → DELETED_IN_GAG(0, T181)
DELETED_IN_GAG(s(T198), tree(s(T199), T181, T180)) → PF_IN_GGAG(T198, T199, T181)
PF_IN_GGAG(T198, T199, T181) → U7_GGAG(T198, T199, T181, lessB_in_gg(T198, T199))
U7_GGAG(T198, T199, T181, lessB_out_gg(T198, T199)) → DELETED_IN_GAG(s(T198), T181)
DELETED_IN_GAG(s(T241), tree(0, T233, T235)) → DELETED_IN_GAG(s(T241), T235)
DELETED_IN_GAG(s(T251), tree(s(T250), T233, T235)) → PG_IN_GGAG(T250, T251, T235)
PG_IN_GGAG(T250, T251, T235) → U9_GGAG(T250, T251, T235, lessB_in_gg(T250, T251))
U9_GGAG(T250, T251, T235, lessB_out_gg(T250, T251)) → DELETED_IN_GAG(s(T251), T235)

The TRS R consists of the following rules:

lessB_in_gg(0, s(T135)) → lessB_out_gg(0, s(T135))
lessB_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, lessB_in_gg(T140, T141))
U2_gg(T140, T141, lessB_out_gg(T140, T141)) → lessB_out_gg(s(T140), s(T141))

The set Q consists of the following terms:

lessB_in_gg(x0, x1)
U2_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PE_IN_GGAG(T121, T122, T125) → U5_GGAG(T121, T122, T125, lessB_in_gg(T121, T122))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U5_GGAG(T121, T122, T125, lessB_out_gg(T121, T122)) → DELETED_IN_GAG(T121, T125)
    The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

  • DELETED_IN_GAG(T121, tree(T122, T125, T124)) → PE_IN_GGAG(T121, T122, T125)
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • PC_IN_GGAG(T159, T158, T162) → U3_GGAG(T159, T158, T162, lessB_in_gg(T159, T158))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U3_GGAG(T159, T158, T162, lessB_out_gg(T159, T158)) → DELETED_IN_GAG(T158, T162)
    The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

  • DELETED_IN_GAG(T158, tree(T159, T160, T162)) → PC_IN_GGAG(T159, T158, T162)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • DELETED_IN_GAG(0, tree(s(T187), T181, T180)) → DELETED_IN_GAG(0, T181)
    The graph contains the following edges 1 >= 1, 2 > 2

  • DELETED_IN_GAG(s(T241), tree(0, T233, T235)) → DELETED_IN_GAG(s(T241), T235)
    The graph contains the following edges 1 >= 1, 2 > 2

  • PF_IN_GGAG(T198, T199, T181) → U7_GGAG(T198, T199, T181, lessB_in_gg(T198, T199))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • PG_IN_GGAG(T250, T251, T235) → U9_GGAG(T250, T251, T235, lessB_in_gg(T250, T251))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U7_GGAG(T198, T199, T181, lessB_out_gg(T198, T199)) → DELETED_IN_GAG(s(T198), T181)
    The graph contains the following edges 3 >= 2

  • U9_GGAG(T250, T251, T235, lessB_out_gg(T250, T251)) → DELETED_IN_GAG(s(T251), T235)
    The graph contains the following edges 3 >= 2

  • DELETED_IN_GAG(s(T198), tree(s(T199), T181, T180)) → PF_IN_GGAG(T198, T199, T181)
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

  • DELETED_IN_GAG(s(T251), tree(s(T250), T233, T235)) → PG_IN_GGAG(T250, T251, T235)
    The graph contains the following edges 2 > 1, 1 > 2, 2 > 3

(29) YES